Termination w.r.t. Q proof of TRS/TRCSREx6_15_AEL02

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__sel₂(s₁(X), cons₂(Y, Z)) -> a__sel₂(mark₁(X), mark₁(Z))
a__sel₂(0, cons₂(X, Z)) -> mark₁(X)
a__first₂(0, Z) -> nil
a__first₂(s₁(X), cons₂(Y, Z)) -> cons₂(mark₁(Y), first₂(X, Z))
a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__sel1₂(s₁(X), cons₂(Y, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__sel1₂(0, cons₂(X, Z)) -> a__quote₁(X)
a__first1₂(0, Z) -> nil1
a__first1₂(s₁(X), cons₂(Y, Z)) -> cons1₂(a__quote₁(Y), a__first1₂(mark₁(X), mark₁(Z)))
a__quote₁(0) -> 01
a__quote1₁(cons₂(X, Z)) -> cons1₂(a__quote₁(X), a__quote1₁(Z))
a__quote1₁(nil) -> nil1
a__quote₁(s₁(X)) -> s1₁(a__quote₁(X))
a__quote₁(sel₂(X, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__quote1₁(first₂(X, Z)) -> a__first1₂(mark₁(X), mark₁(Z))
a__unquote₁(01) -> 0
a__unquote₁(s1₁(X)) -> s₁(a__unquote₁(mark₁(X)))
a__unquote1₁(nil1) -> nil
a__unquote1₁(cons1₂(X, Z)) -> a__fcons₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
a__fcons₂(X, Z) -> cons₂(mark₁(X), Z)
mark₁(sel₂(X1, X2)) -> a__sel₂(mark₁(X1), mark₁(X2))
mark₁(first₂(X1, X2)) -> a__first₂(mark₁(X1), mark₁(X2))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(sel1₂(X1, X2)) -> a__sel1₂(mark₁(X1), mark₁(X2))
mark₁(quote₁(X)) -> a__quote₁(X)
mark₁(first1₂(X1, X2)) -> a__first1₂(mark₁(X1), mark₁(X2))
mark₁(quote1₁(X)) -> a__quote1₁(X)
mark₁(unquote₁(X)) -> a__unquote₁(mark₁(X))
mark₁(unquote1₁(X)) -> a__unquote1₁(mark₁(X))
mark₁(fcons₂(X1, X2)) -> a__fcons₂(mark₁(X1), mark₁(X2))
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(0) -> 0
mark₁(nil) -> nil
mark₁(nil1) -> nil1
mark₁(cons1₂(X1, X2)) -> cons1₂(mark₁(X1), mark₁(X2))
mark₁(01) -> 01
mark₁(s1₁(X)) -> s1₁(mark₁(X))
a__sel₂(X1, X2) -> sel₂(X1, X2)
a__first₂(X1, X2) -> first₂(X1, X2)
a__from₁(X) -> from₁(X)
a__sel1₂(X1, X2) -> sel1₂(X1, X2)
a__quote₁(X) -> quote₁(X)
a__first1₂(X1, X2) -> first1₂(X1, X2)
a__quote1₁(X) -> quote1₁(X)
a__unquote₁(X) -> unquote₁(X)
a__unquote1₁(X) -> unquote1₁(X)
a__fcons₂(X1, X2) -> fcons₂(X1, X2)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__sel₂(s₁(X), cons₂(Y, Z)) -> a__sel₂(mark₁(X), mark₁(Z))
a__sel₂(0, cons₂(X, Z)) -> mark₁(X)
a__first₂(0, Z) -> nil
a__first₂(s₁(X), cons₂(Y, Z)) -> cons₂(mark₁(Y), first₂(X, Z))
a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__sel1₂(s₁(X), cons₂(Y, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__sel1₂(0, cons₂(X, Z)) -> a__quote₁(X)
a__first1₂(0, Z) -> nil1
a__first1₂(s₁(X), cons₂(Y, Z)) -> cons1₂(a__quote₁(Y), a__first1₂(mark₁(X), mark₁(Z)))
a__quote₁(0) -> 01
a__quote1₁(cons₂(X, Z)) -> cons1₂(a__quote₁(X), a__quote1₁(Z))
a__quote1₁(nil) -> nil1
a__quote₁(s₁(X)) -> s1₁(a__quote₁(X))
a__quote₁(sel₂(X, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__quote1₁(first₂(X, Z)) -> a__first1₂(mark₁(X), mark₁(Z))
a__unquote₁(01) -> 0
a__unquote₁(s1₁(X)) -> s₁(a__unquote₁(mark₁(X)))
a__unquote1₁(nil1) -> nil
a__unquote1₁(cons1₂(X, Z)) -> a__fcons₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
a__fcons₂(X, Z) -> cons₂(mark₁(X), Z)
mark₁(sel₂(X1, X2)) -> a__sel₂(mark₁(X1), mark₁(X2))
mark₁(first₂(X1, X2)) -> a__first₂(mark₁(X1), mark₁(X2))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(sel1₂(X1, X2)) -> a__sel1₂(mark₁(X1), mark₁(X2))
mark₁(quote₁(X)) -> a__quote₁(X)
mark₁(first1₂(X1, X2)) -> a__first1₂(mark₁(X1), mark₁(X2))
mark₁(quote1₁(X)) -> a__quote1₁(X)
mark₁(unquote₁(X)) -> a__unquote₁(mark₁(X))
mark₁(unquote1₁(X)) -> a__unquote1₁(mark₁(X))
mark₁(fcons₂(X1, X2)) -> a__fcons₂(mark₁(X1), mark₁(X2))
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(0) -> 0
mark₁(nil) -> nil
mark₁(nil1) -> nil1
mark₁(cons1₂(X1, X2)) -> cons1₂(mark₁(X1), mark₁(X2))
mark₁(01) -> 01
mark₁(s1₁(X)) -> s1₁(mark₁(X))
a__sel₂(X1, X2) -> sel₂(X1, X2)
a__first₂(X1, X2) -> first₂(X1, X2)
a__from₁(X) -> from₁(X)
a__sel1₂(X1, X2) -> sel1₂(X1, X2)
a__quote₁(X) -> quote₁(X)
a__first1₂(X1, X2) -> first1₂(X1, X2)
a__quote1₁(X) -> quote1₁(X)
a__unquote₁(X) -> unquote₁(X)
a__unquote1₁(X) -> unquote1₁(X)
a__fcons₂(X1, X2) -> fcons₂(X1, X2)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A__UNQUOTE1₁(cons1₂(X, Z)) -> MARK₁(X)
MARK₁(first₂(X1, X2)) -> A__FIRST₂(mark₁(X1), mark₁(X2))
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> A__QUOTE₁(Y)
A__QUOTE₁(sel₂(X, Z)) -> MARK₁(Z)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> A__FIRST1₂(mark₁(X), mark₁(Z))
MARK₁(first₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> MARK₁(Z)
A__QUOTE₁(sel₂(X, Z)) -> A__SEL1₂(mark₁(X), mark₁(Z))
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
A__FIRST₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Y)
MARK₁(sel1₂(X1, X2)) -> A__SEL1₂(mark₁(X1), mark₁(X2))
MARK₁(first₂(X1, X2)) -> MARK₁(X1)
MARK₁(first1₂(X1, X2)) -> MARK₁(X1)
MARK₁(first1₂(X1, X2)) -> MARK₁(X2)
A__SEL₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
MARK₁(unquote1₁(X)) -> A__UNQUOTE1₁(mark₁(X))
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__FCONS₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
MARK₁(unquote₁(X)) -> MARK₁(X)
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
MARK₁(fcons₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__UNQUOTE₁(mark₁(X))
MARK₁(unquote1₁(X)) -> MARK₁(X)
A__QUOTE1₁(first₂(X, Z)) -> A__FIRST1₂(mark₁(X), mark₁(Z))
A__QUOTE1₁(cons₂(X, Z)) -> A__QUOTE₁(X)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
MARK₁(s₁(X)) -> MARK₁(X)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
MARK₁(cons1₂(X1, X2)) -> MARK₁(X1)
MARK₁(cons1₂(X1, X2)) -> MARK₁(X2)
MARK₁(quote1₁(X)) -> A__QUOTE1₁(X)
A__FROM₁(X) -> MARK₁(X)
A__SEL₂(0, cons₂(X, Z)) -> MARK₁(X)
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> A__SEL1₂(mark₁(X), mark₁(Z))
MARK₁(sel₂(X1, X2)) -> A__SEL₂(mark₁(X1), mark₁(X2))
A__SEL₂(s₁(X), cons₂(Y, Z)) -> A__SEL₂(mark₁(X), mark₁(Z))
MARK₁(unquote₁(X)) -> A__UNQUOTE₁(mark₁(X))
MARK₁(sel₂(X1, X2)) -> MARK₁(X1)
MARK₁(sel1₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__UNQUOTE1₁(mark₁(Z))
MARK₁(first1₂(X1, X2)) -> A__FIRST1₂(mark₁(X1), mark₁(X2))
MARK₁(sel1₂(X1, X2)) -> MARK₁(X1)
MARK₁(from₁(X)) -> MARK₁(X)
A__QUOTE1₁(cons₂(X, Z)) -> A__QUOTE1₁(Z)
MARK₁(from₁(X)) -> A__FROM₁(mark₁(X))
MARK₁(cons₂(X1, X2)) -> MARK₁(X1)
A__QUOTE1₁(first₂(X, Z)) -> MARK₁(X)
A__UNQUOTE₁(s1₁(X)) -> A__UNQUOTE₁(mark₁(X))
A__QUOTE₁(s₁(X)) -> A__QUOTE₁(X)
MARK₁(fcons₂(X1, X2)) -> A__FCONS₂(mark₁(X1), mark₁(X2))
A__FCONS₂(X, Z) -> MARK₁(X)
MARK₁(sel₂(X1, X2)) -> MARK₁(X2)
A__SEL₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
A__QUOTE1₁(first₂(X, Z)) -> MARK₁(Z)
A__QUOTE₁(sel₂(X, Z)) -> MARK₁(X)
A__UNQUOTE₁(s1₁(X)) -> MARK₁(X)
MARK₁(quote₁(X)) -> A__QUOTE₁(X)
A__SEL1₂(0, cons₂(X, Z)) -> A__QUOTE₁(X)
MARK₁(s1₁(X)) -> MARK₁(X)
MARK₁(fcons₂(X1, X2)) -> MARK₁(X1)

The TRS R consists of the following rules:

a__sel₂(s₁(X), cons₂(Y, Z)) -> a__sel₂(mark₁(X), mark₁(Z))
a__sel₂(0, cons₂(X, Z)) -> mark₁(X)
a__first₂(0, Z) -> nil
a__first₂(s₁(X), cons₂(Y, Z)) -> cons₂(mark₁(Y), first₂(X, Z))
a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__sel1₂(s₁(X), cons₂(Y, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__sel1₂(0, cons₂(X, Z)) -> a__quote₁(X)
a__first1₂(0, Z) -> nil1
a__first1₂(s₁(X), cons₂(Y, Z)) -> cons1₂(a__quote₁(Y), a__first1₂(mark₁(X), mark₁(Z)))
a__quote₁(0) -> 01
a__quote1₁(cons₂(X, Z)) -> cons1₂(a__quote₁(X), a__quote1₁(Z))
a__quote1₁(nil) -> nil1
a__quote₁(s₁(X)) -> s1₁(a__quote₁(X))
a__quote₁(sel₂(X, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__quote1₁(first₂(X, Z)) -> a__first1₂(mark₁(X), mark₁(Z))
a__unquote₁(01) -> 0
a__unquote₁(s1₁(X)) -> s₁(a__unquote₁(mark₁(X)))
a__unquote1₁(nil1) -> nil
a__unquote1₁(cons1₂(X, Z)) -> a__fcons₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
a__fcons₂(X, Z) -> cons₂(mark₁(X), Z)
mark₁(sel₂(X1, X2)) -> a__sel₂(mark₁(X1), mark₁(X2))
mark₁(first₂(X1, X2)) -> a__first₂(mark₁(X1), mark₁(X2))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(sel1₂(X1, X2)) -> a__sel1₂(mark₁(X1), mark₁(X2))
mark₁(quote₁(X)) -> a__quote₁(X)
mark₁(first1₂(X1, X2)) -> a__first1₂(mark₁(X1), mark₁(X2))
mark₁(quote1₁(X)) -> a__quote1₁(X)
mark₁(unquote₁(X)) -> a__unquote₁(mark₁(X))
mark₁(unquote1₁(X)) -> a__unquote1₁(mark₁(X))
mark₁(fcons₂(X1, X2)) -> a__fcons₂(mark₁(X1), mark₁(X2))
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(0) -> 0
mark₁(nil) -> nil
mark₁(nil1) -> nil1
mark₁(cons1₂(X1, X2)) -> cons1₂(mark₁(X1), mark₁(X2))
mark₁(01) -> 01
mark₁(s1₁(X)) -> s1₁(mark₁(X))
a__sel₂(X1, X2) -> sel₂(X1, X2)
a__first₂(X1, X2) -> first₂(X1, X2)
a__from₁(X) -> from₁(X)
a__sel1₂(X1, X2) -> sel1₂(X1, X2)
a__quote₁(X) -> quote₁(X)
a__first1₂(X1, X2) -> first1₂(X1, X2)
a__quote1₁(X) -> quote1₁(X)
a__unquote₁(X) -> unquote₁(X)
a__unquote1₁(X) -> unquote1₁(X)
a__fcons₂(X1, X2) -> fcons₂(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__UNQUOTE1₁(cons1₂(X, Z)) -> MARK₁(X)
MARK₁(first₂(X1, X2)) -> A__FIRST₂(mark₁(X1), mark₁(X2))
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> A__QUOTE₁(Y)
A__QUOTE₁(sel₂(X, Z)) -> MARK₁(Z)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> A__FIRST1₂(mark₁(X), mark₁(Z))
MARK₁(first₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> MARK₁(Z)
A__QUOTE₁(sel₂(X, Z)) -> A__SEL1₂(mark₁(X), mark₁(Z))
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
A__FIRST₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Y)
MARK₁(sel1₂(X1, X2)) -> A__SEL1₂(mark₁(X1), mark₁(X2))
MARK₁(first₂(X1, X2)) -> MARK₁(X1)
MARK₁(first1₂(X1, X2)) -> MARK₁(X1)
MARK₁(first1₂(X1, X2)) -> MARK₁(X2)
A__SEL₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
MARK₁(unquote1₁(X)) -> A__UNQUOTE1₁(mark₁(X))
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__FCONS₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
MARK₁(unquote₁(X)) -> MARK₁(X)
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
MARK₁(fcons₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__UNQUOTE₁(mark₁(X))
MARK₁(unquote1₁(X)) -> MARK₁(X)
A__QUOTE1₁(first₂(X, Z)) -> A__FIRST1₂(mark₁(X), mark₁(Z))
A__QUOTE1₁(cons₂(X, Z)) -> A__QUOTE₁(X)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(X)
MARK₁(s₁(X)) -> MARK₁(X)
A__FIRST1₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
MARK₁(cons1₂(X1, X2)) -> MARK₁(X1)
MARK₁(cons1₂(X1, X2)) -> MARK₁(X2)
MARK₁(quote1₁(X)) -> A__QUOTE1₁(X)
A__FROM₁(X) -> MARK₁(X)
A__SEL₂(0, cons₂(X, Z)) -> MARK₁(X)
A__SEL1₂(s₁(X), cons₂(Y, Z)) -> A__SEL1₂(mark₁(X), mark₁(Z))
MARK₁(sel₂(X1, X2)) -> A__SEL₂(mark₁(X1), mark₁(X2))
A__SEL₂(s₁(X), cons₂(Y, Z)) -> A__SEL₂(mark₁(X), mark₁(Z))
MARK₁(unquote₁(X)) -> A__UNQUOTE₁(mark₁(X))
MARK₁(sel₂(X1, X2)) -> MARK₁(X1)
MARK₁(sel1₂(X1, X2)) -> MARK₁(X2)
A__UNQUOTE1₁(cons1₂(X, Z)) -> A__UNQUOTE1₁(mark₁(Z))
MARK₁(first1₂(X1, X2)) -> A__FIRST1₂(mark₁(X1), mark₁(X2))
MARK₁(sel1₂(X1, X2)) -> MARK₁(X1)
MARK₁(from₁(X)) -> MARK₁(X)
A__QUOTE1₁(cons₂(X, Z)) -> A__QUOTE1₁(Z)
MARK₁(from₁(X)) -> A__FROM₁(mark₁(X))
MARK₁(cons₂(X1, X2)) -> MARK₁(X1)
A__QUOTE1₁(first₂(X, Z)) -> MARK₁(X)
A__UNQUOTE₁(s1₁(X)) -> A__UNQUOTE₁(mark₁(X))
A__QUOTE₁(s₁(X)) -> A__QUOTE₁(X)
MARK₁(fcons₂(X1, X2)) -> A__FCONS₂(mark₁(X1), mark₁(X2))
A__FCONS₂(X, Z) -> MARK₁(X)
MARK₁(sel₂(X1, X2)) -> MARK₁(X2)
A__SEL₂(s₁(X), cons₂(Y, Z)) -> MARK₁(Z)
A__QUOTE1₁(first₂(X, Z)) -> MARK₁(Z)
A__QUOTE₁(sel₂(X, Z)) -> MARK₁(X)
A__UNQUOTE₁(s1₁(X)) -> MARK₁(X)
MARK₁(quote₁(X)) -> A__QUOTE₁(X)
A__SEL1₂(0, cons₂(X, Z)) -> A__QUOTE₁(X)
MARK₁(s1₁(X)) -> MARK₁(X)
MARK₁(fcons₂(X1, X2)) -> MARK₁(X1)

The TRS R consists of the following rules:

a__sel₂(s₁(X), cons₂(Y, Z)) -> a__sel₂(mark₁(X), mark₁(Z))
a__sel₂(0, cons₂(X, Z)) -> mark₁(X)
a__first₂(0, Z) -> nil
a__first₂(s₁(X), cons₂(Y, Z)) -> cons₂(mark₁(Y), first₂(X, Z))
a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__sel1₂(s₁(X), cons₂(Y, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__sel1₂(0, cons₂(X, Z)) -> a__quote₁(X)
a__first1₂(0, Z) -> nil1
a__first1₂(s₁(X), cons₂(Y, Z)) -> cons1₂(a__quote₁(Y), a__first1₂(mark₁(X), mark₁(Z)))
a__quote₁(0) -> 01
a__quote1₁(cons₂(X, Z)) -> cons1₂(a__quote₁(X), a__quote1₁(Z))
a__quote1₁(nil) -> nil1
a__quote₁(s₁(X)) -> s1₁(a__quote₁(X))
a__quote₁(sel₂(X, Z)) -> a__sel1₂(mark₁(X), mark₁(Z))
a__quote1₁(first₂(X, Z)) -> a__first1₂(mark₁(X), mark₁(Z))
a__unquote₁(01) -> 0
a__unquote₁(s1₁(X)) -> s₁(a__unquote₁(mark₁(X)))
a__unquote1₁(nil1) -> nil
a__unquote1₁(cons1₂(X, Z)) -> a__fcons₂(a__unquote₁(mark₁(X)), a__unquote1₁(mark₁(Z)))
a__fcons₂(X, Z) -> cons₂(mark₁(X), Z)
mark₁(sel₂(X1, X2)) -> a__sel₂(mark₁(X1), mark₁(X2))
mark₁(first₂(X1, X2)) -> a__first₂(mark₁(X1), mark₁(X2))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(sel1₂(X1, X2)) -> a__sel1₂(mark₁(X1), mark₁(X2))
mark₁(quote₁(X)) -> a__quote₁(X)
mark₁(first1₂(X1, X2)) -> a__first1₂(mark₁(X1), mark₁(X2))
mark₁(quote1₁(X)) -> a__quote1₁(X)
mark₁(unquote₁(X)) -> a__unquote₁(mark₁(X))
mark₁(unquote1₁(X)) -> a__unquote1₁(mark₁(X))
mark₁(fcons₂(X1, X2)) -> a__fcons₂(mark₁(X1), mark₁(X2))
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(0) -> 0
mark₁(nil) -> nil
mark₁(nil1) -> nil1
mark₁(cons1₂(X1, X2)) -> cons1₂(mark₁(X1), mark₁(X2))
mark₁(01) -> 01
mark₁(s1₁(X)) -> s1₁(mark₁(X))
a__sel₂(X1, X2) -> sel₂(X1, X2)
a__first₂(X1, X2) -> first₂(X1, X2)
a__from₁(X) -> from₁(X)
a__sel1₂(X1, X2) -> sel1₂(X1, X2)
a__quote₁(X) -> quote₁(X)
a__first1₂(X1, X2) -> first1₂(X1, X2)
a__quote1₁(X) -> quote1₁(X)
a__unquote₁(X) -> unquote₁(X)
a__unquote1₁(X) -> unquote1₁(X)
a__fcons₂(X1, X2) -> fcons₂(X1, X2)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.